COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	HELP
C00024 ENDMK
C⊗;
HELP
"This program is designed to be used as a tool for verification
of properties of PASCAL programs presented to it, along with
lemmas about thoso programs.  The most commonly used upper level
command is READ.  Type 'HELP WHAT;' for a list of help commands.
For help on topic X, assuming help data exists, type 'HELP X;'."

WHAT
"HELP messages are available for the following:
ALIAS
BREAK
BUG
COMMANDS
DELRFILE, DELRULE
DOCUMENTATION
DUMP, DUMPVC, DUMPRULE, DUMPINTERNAL, DUMPSYMBOLS
INTERRUPT
LISP
LOAD, LOADVC, LOADRULE, LOADSYMBOLS
MANUAL
NEWS
PARSE
PREVIOUS
PRINTVC
READ, READVC
SHOW
SIMPINIT
SIMPLIFY
STATUS
SWITCHES
SYSTEM
TOPLEVEL
VC
This file (which contains all the help routines) is NEWVER.HP2[1,3]."

ALIAS
"This command is used to change the default disk area used by commands
that read or write files (DUMP, READ and LOAD commands, at present).
'ALIAS EX,VER;', for example, will set [EX,VER] as the default area
for these commands.  Of course, you can override the default by
specifying the area explicitly in one of these commands.  'ALIAS;'
will display your current default area."

BREAK
"In case the verifier ends up in a LISP error and stops at a breakpoint
you have to type <control>-P to get back to the toplevel."

BUG
"The BUG feature is provided to help verifier hackers make changes to
syntax, semantics, etc.  There are two user commands, (SETBUG <number>)
and (RESETBUG <number>), which set and then reset the bug with the
appropriate number.  See MEMO[VCG,RAK] to see which bugs currently
exist and what they do. These commands are available at LISP level
only."

COMMANDS
"The following commands are available:
READ commands: READ, READVC;
LOAD commands: LOAD(VC/RULE/TABLE);
DUMP commands: DUMP(VC/RULE/TABLE);
SIMPLIFY;
ALIAS;
Display commands: SHOW, STATUS, HELP;
DELRFILE, DELRULE;
LISP.
For more information type HELP followed by the command, or read the
file TOPLEV[DOC,VER]."

DOCUMENTATION
"Files intended to be documentation on the verifier or portions 
thereof are kept in the directory [DOC,VER].  You might try looking
there for things.  Don't be too surprised if some large gaps exist.
The system toplevel is documented in TOPLEV[DOC,VER].
Here are a few other random places:
MEMO[VCG,RAK] -- about the parser, Pascal, etc.
SSEM[VCG,RAK] -- page 2 explains the structure of the symbol table
VERIFY.DOC[DOC,VER] -- Details about LOADVC, LOADRULE, DUMPVC, DUMPRULE,
	ALIAS.   Also information about examples in [EX,VER], hackery
	information, etc. "

DUMP
"The command DUMP is a combination of DUMPVC and DUMPRULE.
'DUMP FOO;' is equivalent to 'DUMPVC FOO;' followed by 'DUMPRULE FOO;'.
Note that the filename argument for DUMP must not have an extension."

DUMPINTERNAL
"This command is either (DUMPINTERNAL T) or (DUMPINTERNAL NIL) to
turn the facility on or off; default is NIL.  DUMPINTERNAL causes
internal format output by the parser to be placed in the symbol
table for each procedure or function parsed.  It is generally only
useful in conjunction with dumping the symbol table (see DUMPSYMBOLS)
and the VC command (see VC). THIS COMMAND IS AVAILABLE AS A LISP
FUNCTION ONLY."

DUMPRULE
"The command DUMPRULE is used to dump a 'compiled' rulefile to disk.
It allows use of the standalone simplifier, VPROVE, and also saves
parse time because rulefiles need only be parsed once, then dumped.
The default filename is VERIFY.CRL in your aliased area (which is
affectes by the ALIAS command).  This command should 
be used in conjunction with LOADRULE, which loads these 'compiled'
rulefiles.   Thus, you can parse a rulefile using VCGEN or VERIFY, 
do a DUMPRULE, and then load it via LOADRULE into either VPROVE 
or VERIFY.    Examples:  'DUMPRULE SORT;' makes SORT.CRL.
'DUMPRULE FOO.CRL[VER,BAR];' makes FOO.CRL[VER,BAR].   If more than
one rulefile exists, it will dump the most recent one parsed.  You may
also specify a rulefile name to DUMPRULE, as in 'DUMPRULE SORT, SORTRULES;'.
LOADRULE is used to load in these files (the same naming defaults apply)."

DUMPSYMBOLS
"The command DUMPSYMBOLS is optionally followed by a file in the
same format as PARSE.  It instructs the parser to dump code to that
file that will permit reloading the symbol table environment of all
the procedures in the file.  (DUMPSYMBOLS) turns off dumping.  So
does any subsequent attempt to load a symbol table file.  See
LOADSYMBOLS for information on how to load a symbol table.
This command is presently only available as a LISP function."

DUMPVC
"The command DUMPVC is used to dump verification conditions into a
file.  It is usefule because it allows use of the standalone prover,
VPROVE, and because it saves parsing time by storing the VCs in their
internal format. The default extension is .CVC; thus 'DUMPVC FOO;'
writes on a file FOO.CVC.  If no filename is given, VERIFY.CVC in your
aliased area (which can be set via the ALIAS command) is used.  LOADVC
is used to load these files.  Thus, a program may be parsed with VCGEN
or VERIFY, and the VCs dumped with DUMPVC.  The LOADVC may be used to
load the VCs into VPROVE or VERIFY for later use.  Examples:
'DUMPVC FOO;' puts the compiled VCs into FOO.CVC in your aliased area.
'DUMPVC FOO.CVC[VER,BAR];' puts them in FOO.CVC[VER,BAR].  LOADVC has
a corresponding syntax."

INTERRUPT
"A computation can be abandonned by typing <escape>I , which will
return you to the verifier toplevel (after doing some clean-up)."

LISP
"Although this is primarily a program verifier, it exists in a
MACLSP environment.  This means that the general facilities of
such LISP are available.  The command 'LISP;' returns control to the
MACLISP toplevel. In order to get back to the non-LISP toplevel type
'(RESUME)'.  The file VERIFY.DOC[DOC,VER] contains some advice
about recovery from errors, etc. in MACLISP."

LOADRULE
"The command LOADRULE is used to load in files created with DUMPRULE.
See DUMPRULE for further information."

LOADSYMBOLS
"The command LOADSYMBOLS must be followed by two items: first a
procedure name and then a file.  The system will turn off symbol
table dumping (if it is on), clear the symbol table, and then attempt
to load the symbol table environment of the procedure specified from
the file given.  The format of the file name is the same as that of
the PARSE command. See DUMPSYMBOLS for information on how to create
a file that contains symbol table information. This command is presently
only available as a LISP function."

LOADVC
"The command LOADVC is used to load in files created by DUMPVC.
See DUMPVC for further information."

MANUAL
"Unfortunately, manual mode is not up yet.  If you want to
implement it, talk to WLS."

NEWS
"The STATUS command displays info about VCs and rules loaded.
SHOW displays the values of system switches.
DELRULE rule deletes rule 'rule', and 'DELRFILE rfile;' deletes
the rulefile 'rfile'. For more info type 'HELP STATUS;' etc."
 
PARSE
"You should use READ instead of the internal PARSE command !!
The command (PARSE) accepts input from the teletype. (PARSE X)
will try to take input from the file X.  Here are some examples
for taking files with two word names and from another directory
(here p,pn is programmer,project and X Y is the two word file name
X.Y): (PARSE X Y), (PARSE X (P,PN)), and (PARSE X Y (P,PN))  .  
The parser calls the verification condition generator, but does
not do simplification.  For this, the command SIMPLIFY must be
used. The syntactic scan and semantic routines should NEVER
bomb out, no matter what string you give them.  If they do,
send a note to RAK and SAVE the program!!!"

PREVIOUS
"The command (PREVIOUS <positive integer>) has meaning when a
syntax scan finds a syntax error.  It will print out as many
tokens preceding the syntax error as it is asked (if there are
that many).  (PREVIOUS 10) is called in the errorhandling.  As
the number of tokens requested increases, time to find them can
go up alarmingly. After an error and before parsing something
else, previous may be called as many times as desired."

PRINTVC
"The command PRINTVC is used to output unsimplified verfication
conditions.  'PRINTVC;' prints out all of these on the
terminal.  'PRINTVC X;' prints out all of the VC's for procedure X.
'PRINTVC X 3;' prints the third VC for procedure X.
'PRINTVC → F;' prints out all VC's to file F, which is replaced
if it was previously present.  'PRINTVC X → F;' prints out all
VC's for procedure X on file F.
OUTPUT TO FILES IS NOT IMPLEMENTED IN THE CURRENT SYSTEM !!!
The outer block of a program is currently called MAIN. It will
remove VC's for a procedure named MAIN, if one is present!"

READ
"The READ command parses input (programs or rules).
'READ;' accepts input from the teletype.
'READ X;' will try to take input from the file X, where X is
a standard filename (e.g. FOO.BAR[DOT,WIZ]).
The parser calls the verification condition generator, but does
not do simplification.  For this, the command SIMPLIFY must be
used. The syntactic scan and semantic routines should NEVER
bomb out, no matter what string you give them.  If they do,
send a note to RAK and SAVE the program!!!
READ knows about the extension .VC; 'READ FOO.VC;' is equivalent
to the command 'READVC FOO;'."

READVC
"The command READVC is used to input verification conditions in
external format that were dumped by either a PRINTVC, SIMPLIFY,
or RESIMPLIFY command.  READVC takes a file name in the same
format as READ. The filename extesnion .VC can be omitted.
READVC will expect that file to be a list of
VCs in external format as output by the system.  All previously
existing VCs are deleted and all VCs in the file are loaded.
Note that you may use READVC to continue from a partially
simplified VC dumped by SIMPLIFY.  When used from the terminal,
READVC expects a list of one or more of the form NAME VC,
terminated by a period.  It is probably best to enclose the 
last VC in parenthesis, as the final period is frequently
mistaken for a record-field indicator."


SIMPINIT
"The SIMPINIT command is used to reinitialize the simplifier.  It
should be called whenever a simplification has terminated incorrectly,
for example, in a breakpoint.   In MACLISP, incant <control>G to 
escape from a breakpoint.   In general use, you will never have to do
(SIMPINIT). SIMPINIT is not available at the command toplevel."

SIMPLIFY
"The command SIMPLIFY is used to call the simplifier and output
simplified verification conditions.  The procedure and output
file specifications are the same as for PRINTVC.  Use
'HELP PRINTVC;' to see these conventions."

SHOW
"The command SHOW displays the values of system switches. 'SHOW;'
displays all switches, 'SHOW switch;' displays the value of
switch (if it is a switch). To see the list of available switches,
type 'HELP SWITCHES;'."

STATUS
"The command STATUS prints out a list of the vc's, rulefiles and
rules currently loaded. STATUS takes no arguments."

SWITCHES
"The verifier is controlled by some switches whose values can be set
by the user.  The following list gives their names and the type of
their values (natnum: an integer greater than or equal to zero; bool:
T or NIL):
RULE		bool	enable rule handler.
DEPTHTALK	bool	signal whenever a depth bound is reached.
PROOFDEPTH	natnum	maximum backwards proof depth.
ASSERTDEPTH	natnum	maximum forwards assertion depth.
CASEDEPTH	natnum	maximum depth of nesting of forwards cases.
SHOWFACT	bool	enable assertion display during proof.
SHOWGOAL	bool	enable subgoal display during proof.
SHOWTEST	bool	enable display of tests made during proof.
SUMMATCH 	bool	enable special sum matching: extra subspace
			instance.
TRACE		bool	enable proof tracing.
TRACEVC		bool	enable display of intermediate VC during proof.
TRACEFACT	bool	enable display of assertions made in trace
				output (works only if TRACE is set).
Current default values can be found out with the SHOW command."

SYSTEM
"The verification system consists of the parser, the verification
condition generator, and the prover parts. The system comes in three
varieties: the full system, the vc-generator, called VCGEN, consisting
of parser and VCG, and the prover, called VPROVE. It is advisable to
keep down core size by using VCGEN, dumping VC's and rules onto files
and loading these into VPROVE.  If a particular function is not
available in a subsystem (like READ in VPROVE) you will get an
appropriate message."

TOPLEVEL
"The toplevel of the verifier consists of a read-eval-loop that parses
and executes various commands. A system command consists of a command
keyword, possibly followed by some arguments, and a terminating ;. The
semicolon must always be present (if it is omitted, the system will
prompt you with '>' to indicate that more input is expected). The
toplevel commands are documented in the file TOPLEV[DOC,VER].
Explanations are also provided by the HELP feature: type 'HELP
<command-keyword>;' - 'HELP WHAT;' gives a list of keywords."

VC
"This command is not intended for general use. It is only available as
a LISP function.
(VC @procname) sets up and calls the verification condition generator.
It requires that the name be a procedue or function, with internal
format dumped by the parser.  This dumping usually requires that
DUMPINTERNAL be set (which see) when parsing the procedure."

END